Nuprl Lemma : search_wf
4,23
postcript
pdf
k
:
,
P
:(
k
). search(
k
;
P
)
(
k
+1)
latex
Definitions
,
search(
k
;
P
)
,
primrec(
n
;
b
;
c
)
,
i
<
j
,
if
b
t
else
f
fi
,
,
i
j
<
k
,
A
B
,
P
&
Q
,
A
,
False
,
P
Q
,
x
:
A
.
B
(
x
)
,
t
T
,
{
i
..
j
}
Lemmas
ifthenelse
wf
,
lt
int
wf
,
int
seg
wf
,
primrec
wf
,
nat
wf
,
bool
wf
origin
k:
, P:(k
). search(k;P) 
(k+1) k:, P:(k). search(k;P) (k+1) 
j
t else f fi
j < kB
A
Qx:A. B(x) T
}